Inference at * 1 1 
Iof proof for Lemma before-hd:



1. T : Type
2. L : T List
3. 0 < ||L||
4. no_repeats(T;L)
5. x : T
6. x before hd(L)  L
7. x, y:T. x before y  L  ((x = y))
8. (x = hd(L))
9. hd(L) before x  L
  False 

latex

 by InteriorProof ((FLemma `l_before_transitivity` [6;9]) 
CollapseTHEN (MaAuto)) 

latex

C1: 

C1: 10. x before x  L
C1:   False
C.

Definitions	t  T, , #$n, ||as||, i  j , s = t, Void, x before y  l, L1  L2, hd(l), x:A. B(x), x:A  B(x), no_repeats(T;l), A, x:A. B(x), P  Q, x:AB(x), a < b, type List, False, Type
Lemmas	l before transitivity